Add CI for spell check and other linters #231

k4rtik · 2022-03-23T22:12:55Z

Following up with #173 (comment) and #197 (comment)

The linters currently point out some typos etc, see https://github.com/k4rtik/platform/runs/5667821385?check_suite_focus=true#step:4:254 but I have not fixed them in this PR to test the tool's auto PR support for those fixes.

Once this PR is merged, we may want to change VALIDATE_ALL_CODEBASE: true to VALIDATE_ALL_CODEBASE: ${{ github.event_name == 'push' && github.ref == 'refs/heads/main' }} so that CI only tests the new changes.

I have also disabled certain linters that may involve stylistic choices, namely:

DISABLE_LINTERS:
  - SPELL_CSPELL
  - ACTION_ACTIONLINT
  - BASH_SHELLCHECK
  - C_CPPLINT
  - BASH_SHFMT
  - MARKDOWN_MARKDOWNLINT

I will let you decide about enabling them.

k4rtik · 2022-03-23T22:16:43Z

Lo, it ran but needs permission to create a PR:

Identified PR#231 from environment
[GitHub Comment Reporter] Unable to post pull request comment: 403 {"message": "Resource not accessible by integration", "documentation_url": "https://docs.github.com/rest/reference/issues#create-an-issue-comment"}.
To enable this function, please :

Create a Personal Access Token (https://docs.github.com/en/free-pro-team@latest/github/authenticating-to-github/creating-a-personal-access-token)

Create a secret named PAT with its value on your repository (https://docs.github.com/en/free-pro-team@latest/actions/reference/encrypted-secrets#creating-encrypted-secrets-for-a-repository)3. Define PAT={{secrets.PAT}} in your GitHub action environment variables

MSoegtropIMC · 2022-03-24T08:18:59Z

@k4rtik : thanks I appreciate it - I belong to those people who have difficulties with languages which don't come with compilers.

I will take care of the access token.

MSoegtropIMC · 2022-03-24T08:44:50Z

@k4rtik : is there a way to avoid the chmod of the files in the shell-scripts folder? None of these files is intended to be called directly - they are all intended to be sourced. So the access mode 644 is intentional and a 755 mode would be more confusing than helpful.

MSoegtropIMC · 2022-03-24T08:59:00Z

Another issue is that issues in the auto generated Readme files should be flagged, but not corrected. All errors in auto generated files must be fixed somewhere else.

MSoegtropIMC · 2022-03-24T09:00:44Z

I added the secret, but it didn't do anything I guess because in the PR all changes are already fixed. So I guess to test the PR I need to undo all these changes?

MSoegtropIMC · 2022-03-24T10:01:22Z

@k4rtik : a last comment - can you please factor out the suggested changed from the CI procedure? The CI procedure I am happy to merge as is, but most of the suggested changes not.

"Improve performance by switching to python flavor" commit 184db9e.

k4rtik · 2022-03-24T12:30:05Z

@k4rtik : is there a way to avoid the chmod of the files in the shell-scripts folder? None of these files is intended to be called directly - they are all intended to be sourced. So the access mode 644 is intentional and a 755 mode would be more confusing than helpful.

Yes, pushing this change. Sorry about the confusion.

Another issue is that issues in the auto generated Readme files should be flagged, but not corrected. All errors in auto generated files must be fixed somewhere else.

They seem flagged, but there is still some permissions issue, see the error:

[GitHub Status Reporter] Error posting Status for MARKDOWNwith markdown-table-formatter: 401
GitHub API response: {"message":"Bad credentials","documentation_url":"https://docs.github.com/rest"}
[Text Reporter] Generated TEXT report: /github/workspace/report/linters_logs/SUCCESS-MARKDOWN_MARKDOWN_TABLE_FORMATTER.log

I think this might be because of the change you made at 64269d4#diff-206ce5348d308a71dab8cdc132d6dc2babebc80b94a707a45a744909ed9367d4L44

-    GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+    GITHUB_TOKEN: ${{ secrets.PAT_LINT_SPELL }}

According to the doc, this does not need to be touched. "GITHUB_TOKEN" is automatically set by GitHub.

I added the secret, but it didn't do anything I guess because in the PR all changes are already fixed. So I guess to test the PR I need to undo all these changes?

I think this will also require that the correct GITHUB_TOKEN is passed. I am reverting that small change. The changes are not in the PR. :)

can you please factor out the suggested changed from the CI procedure? The CI procedure I am happy to merge as is, but most of the suggested changes not.

To be clear, the only suggested changes that I included in the PR were file permissions, and those that could not be fixed automatically such as bad links/were leading to false positives such as _CoqProject. I took another look but there is nothing else to factor out.

We can decide about keeping automatic fixing of suggestions once we test this feature out.

MSoegtropIMC · 2022-03-24T12:39:55Z

@k4rtik : thanks:

regarding factoring: I want to strictly separate the CI procedure as such (I would think 2 files) and any changes it produces. E.g. the link changes in the .MD files should also be done differently (by creating a new section which covers the two). But any way, introducing these checks in CI and actually fixing them should be separate, independent steps.

MSoegtropIMC · 2022-03-24T12:40:35Z

P.S.: Please abort the main CI processes when you do changes - for this PR only the new CI step needs to run.

k4rtik · 2022-03-24T12:40:38Z

Hi @MSoegtropIMC can you manually cancel these platform CI runs, ie, all except the Megalinter one? As it may not get queued until much later.

k4rtik · 2022-03-24T12:42:06Z

Is there a way for me to abort them? I don't think I have permission.

Or did you mean to disable them while making the PR?

MSoegtropIMC · 2022-03-24T12:45:32Z

Ah I forgot that you don't have permission for this. I think it is better then to disable them for the PR - I will then piggy back the PR and reenable it before I merge.

k4rtik · 2022-03-24T13:12:06Z

Hi @MSoegtropIMC

I am getting this error with my latest change:

Error: Input required and not supplied: token

Can you please double-check if the personal access token you created is called PAT_LINT_SPELL?

Unsure what's happening here.

MSoegtropIMC · 2022-03-24T13:40:39Z

AFAIK the secrets are not available in PRs from forks.

MSoegtropIMC · 2022-03-24T13:45:44Z

doc/README_Linux.md

@@ -77,7 +77,7 @@ This method is intended for experienced users, who may want to use opam to insta
  - Debian, Ubuntu:       sudo apt-get install build-essential
  - CentOS, RHEL, Fedora: sudo dnf groupinstall "Development Tools"
  - OpenSuse:             sudo zypper in -t pattern devel_C_C++
- For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos) below.
+- For CentOS and possibly RHEL some additional steps are required, see [CentOS](#centos-enable-sudo-for-current-user) below.


This change is not ok. Instead there should be a section "CentOS" which covers the two subsections.

MSoegtropIMC · 2022-03-24T13:46:12Z

doc/README_macOS.md

@@ -22,8 +22,6 @@ right click the `Coq_Platform` app in `/Applications` in Finder and select `open
 - In case you want to use the installed `coqc` from the command line, please add the folder `/Applications/Coq_Platform_2022.01.0.app/Contents/Resources/bin` to your `PATH`.
 - If you want to inspect the installed content, right click the `Coq_Platform` app in `/Applications` in Finder and select `Show Package Contents`.

-A note to lecturers: it is easy to create a customized Windows installer from an opam switch - see [Customized Installers](#customized-installers)


This change is not OK - it just deletes a useful point.

I stripped it because this read me is about macOS and this point is included in windows read me.

Indeed - but the point is the same for MacOS, so the right fix would be to add the corresponding section. So please leave this in and just write "MacOS" instead of "Windows", remove the link and create an issue to add the section.

MSoegtropIMC · 2022-03-24T13:47:40Z

doc/README~8.13~2021.02.md

@@ -248,7 +248,7 @@ The **full level** contains the following packages:
      (<a href='https://github.com/HoTT/HoTT/issues'>bug reports</a>)
      (<a href='https://coq.inria.fr/opam/released/packages/coq-hott/coq-hott.8.13/opam'>opam package</a>)
    </dd>
-    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to _CoqProject:<br>   -arg -noinit<br>   -arg -indices-matter</dd>
+    <dt><b>description</b></dt><dd>To use the HoTT library, the following flags must be passed to coqc:<br>   -noinit -indices-matter<br>To use the HoTT library in a project, add the following to <code>_CoqProject</code>:<br>   -arg -noinit<br>   -arg -indices-matter</dd>


Can such changes be removed? It somehow makes sense, but these files are auto generated from Opam metadata, and I don't want to get correction PRs each time i update the ReadMe files.

MSoegtropIMC · 2022-03-24T13:53:30Z

@k4rtik : can you please do the requested changes - or alternatively remove the ReadMe files from the commit.

Also can you please change the bad charter link in [maintainer_scripts/create_readme.sh] - I think this should go together with the same change in the auto generated files.

I will then take it from there - I guess this will run only on main (which I think is good enough).

k4rtik · 2022-03-24T14:15:49Z

AFAIK the secrets are not available in PRs from forks.

In that case let me try testing these features on my fork directly and then I will send a PR later.

k4rtik and others added 6 commits March 24, 2022 09:54

Add a CI for spelling check

a4013b6

Enable spell check on everything to test

94bacec

One more try

88f7c37

Disable unneeded linters

8367162

Improve performance by switching to python flavor

184db9e

Set secret for creating PR

64269d4

MSoegtropIMC force-pushed the spell-ci branch from 670d7f9 to 64269d4 Compare March 24, 2022 08:56

k4rtik added 2 commits March 24, 2022 07:10

Restore file permissions by reverting part of the commit

b8b061a

"Improve performance by switching to python flavor" commit 184db9e.

Fix GITHUB_TOKEN

614a179

Restore token for GH action

fc8c136

k4rtik added 2 commits March 24, 2022 07:59

Try again using PAT environment variable

7007a6e

This is mysterious

026fa90

MSoegtropIMC requested changes Mar 24, 2022

View reviewed changes

k4rtik marked this pull request as draft March 24, 2022 14:13

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add CI for spell check and other linters #231

Add CI for spell check and other linters #231

k4rtik commented Mar 23, 2022

k4rtik commented Mar 23, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC Mar 24, 2022

MSoegtropIMC Mar 24, 2022

k4rtik Mar 24, 2022

MSoegtropIMC Mar 24, 2022

MSoegtropIMC Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

Add CI for spell check and other linters #231

Are you sure you want to change the base?

Add CI for spell check and other linters #231

Conversation

k4rtik commented Mar 23, 2022

k4rtik commented Mar 23, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022

MSoegtropIMC commented Mar 24, 2022

MSoegtropIMC Mar 24, 2022

Choose a reason for hiding this comment

MSoegtropIMC Mar 24, 2022

Choose a reason for hiding this comment

k4rtik Mar 24, 2022

Choose a reason for hiding this comment

MSoegtropIMC Mar 24, 2022

Choose a reason for hiding this comment

MSoegtropIMC Mar 24, 2022

Choose a reason for hiding this comment

MSoegtropIMC commented Mar 24, 2022

k4rtik commented Mar 24, 2022